$\forall$$k$:Knd, $f$, $g$:Top.
\\[0ex]($\neg$($\uparrow$islocal($k$))) $\Rightarrow$ (kindcase($k$; $a$.$f$($a$); $l$,$t$.$g$($l$,$t$) ) $\sim$ $g$(lnk($k$),tag($k$)))